1. Field of the Invention
This invention relates to the design of large and complex hardware or hardware-software combinations. More particularly, this invention discloses witness graphs, and their use in design validation in the automatic generation of test benches and in a coverage metric.
2. Background and Related Art
The following papers provide useful background information, for which they are incorporated herein by reference in their entirety, and are selectively referred to in the remainder of this disclosure by their accompanying reference numbers in angle brackets (i.e., <1> for the first numbered paper by Balarin and Sangiovanni-Vincentelli):    1. F. Balarin and A. Sangiovanni-Vincentelli, “An iterative approach to language containment,” In Proceedings of the International Conference on Computer-Aided Verification, volume 697 of Lecture Notes in Computer Science, pages 29–40, 1993.    2. R. K. Brayton et al. “VIS: A system for verification and synthesis”, In R. Alur and T. Henzinger, editors, Proceedings of the Internation Conference on Computer-Aided Verification, volume 1102, pages 428–432. Springer-Verlag, June 1996.    3. R. E. Bryant, “Graph-based algorithms for Boolean function manipulation”, IEEE Transactions on Computers, C-35(8): 677–691, August 1986.    4. J. R. Burch, E. M. Clarke, D. E. Long, K. L. McMillan, and D. L. Dill, “Symbolic model checking for sequential circuit verification”, IEEE Transactions on Computer-Aided Design, 13(4): 401–424, April 1994.    5. A. K. Chandra, V. S. Iyengar, D. Jameson, R. Jawalekar, I. Nair, B. Rosen, M. Mullen, J. Yoor, R. Armoni, D. Geist, and Y. Wolfsthal, “Avpgen—a test case generator for architecture verification”, IEEE Transactions on VLSI Systems, 6(6), June 1995.    6. E. M. Clarke, E. A. Emerson, and A. P. Sistla, “Automatic verification of finite-state concurrent systems using temporal logic specifications”, ACM Transactions on Programming Languages and Systems, 8(2): 244–263, April 1986.    7. E. M. Clarke, O. Grumberg, Y. Lu, and H. Veith, “Counterexample-guided abstraction refinement”, In Proceedings of the International Conference on Computer-Aided Verification, volume 1855 of Lecture Notes in Computer Science, pages 154–169, 2000.    8. F. Fallah, S. Devadas, and K. Keutzer, “Functional vector generation for HDL models using linear programming and 3-Satisfiability”, In Proceedings of the Design Automation Conference, pages 528—533, San Francisco, Calif., June 1998.    9. M. Ganai, A. Aziz, and A. Kuehlmann, “Augmenting simulation with symbolic algorithms”, In Proceedings of the Design Automation Conference, June 1999.    10. D. Geist, M. Farkas, A. Landver, Y. Lichtenstein, S. Ur, and Y. Wolfsthal, “Coverage-directed test generation using symbolic techniques”, In Proceedings of the International Conference on Formal Methods in CAD, pages 143–158, November 1996.    11. R. C. Ho, C. H. Yang, M. A. Horowitz, and D. L. Dill, “Architecture validation for processors”, In Proceedings of the 22nd Annual International Symposium on Computer Architecture, June 1995.    12. Y. Hoskote, T. Kam, P.-H. Ho, and X. Zhao, “Coverage estimation for symbolic model checking”, In Proceedings of the Design Automation Conference, pages 300–305, June 1999.    13. Y. Hoskote, D. Moundanos, and J. A. Abraham, “Automatic extraction of the control flow machine and application to evaluating coverage of verification vectors”, In Proceedings of the International Conference on Computer Design, pages 532–537, October 1995.    14. C.-Y. Huang and K.-T. Cheng, “Assertion checking by combined word-level ATPG and modular arithmetic constraint-solving techniques”, In Proceedings of the Design Automation Conference, pages 118–123, 2000.    15. C. N. Ip, “Using symbolic analysis to optimize explicit reachability analysis”, In Proceedings of Workshop on High Level Design Validation and Test, 1999.    16. S. Katz, O. Grumberg, and D. Geist, “Have I Written Enough Properties?—a method of comparison between specification and implementation”, In Proceedings of Correct Hardware Design and Verification Methods (CHARME), volume 1703 of Lecture Notes in Computer Science, pages 280–297, September 1999.    17. A. Kuehlmann, K. McMillan, and R. K. Brayton, “Probabilistic state space search”, In Proceedings of the International Conference on Computer-Aided Design, 1999.    18. R. P. Kurshan, Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach, Princeton University Press, 1995.    19. W. Lee, A. Pardo, J. Jang, G. Hachtel, and F. Somenzi, “Tearing based abstraction for CTL model checking”, In Proceedings of the International Conference on Computer-Aided Design, pages 76–81, San Jose, Calif., November 1996.    20. J. Lind-Nielsen and H. R. Anderson, “Stepwise CTL model checking of state/event systems”, In Proceedings of the International Conference on Computer-Aided Verification, volume 1633 of Lecture Notes in Computer Science, pages 316–327. Springer-Verlag, 1999.    21. D. E. Long, Model Checking, Abstraction and Modular Verification, PhD thesis, School of Computer Science, Carnegie Mellon University, Pittsburgh, Pa., July 1993.    22. K. L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers, 1993.    23. A. Pardo and G. Hachtel, “Automatic abstraction techniques for propositional μ-calculus model checking”, In Proceedings of the International Conference on Computer Aided Verification, volume 1254 of Lecture Notes in Computer Science, pages 12–23, June 1997.    24. R. Sumners, J. Bhadra, and J. Abraham, “Improving witness search using orders on states”, In Proceedings of the International Conference on Computer Design, pages 452–457, 1999.    25. Synopsys, Inc. VERA System Verifier, http://www.synopsys.com/products/vera/vera.html.    26. TransEDA, Inc. Verification Navigator, http://www.transeda.com.    27. Verisity Design, Inc. Specman Elite, http://www.verisity.com/html/specmanelite.html.    28. K. Wakabayashi, “C-based Synthesis Experiences with a Behavior Synthesizer “Cyber” ”, In Proceedings of the Design Automation and Test in Europe (DATE) Conference, pages 390–393, 1999.    29. C. Han Yang and David L. Dill, “Validation with guided search of the state space”, In Proceedings of the Design Automation Conference, June 1998.    30. J. Yuan, J. Shen, J. Abraham, and A. Aziz, “On combining formal and informal verification”, In Proceedings of the International Conference on Computer-Aided Verification, volume 1254 of Lecture Notes in Computer Science, pages 376–387, June 1997.